% Correct this command, adding asynchrony and passivation
\newcommand{\ccsb}{\ensuremath{\mathrm{CCS}_{!}}\xspace}





\section{Passivation in CCS with Replication}

\subsection{The Calculus}\label{sec:calculi}


\begin{definition}[\ccsb]\label{primadef}
%{\bf (finite cor)}
Let $Name$, ranged over by $x$, $y$, $\ldots$,
be a denumerable set of channel names.
%We use $\tilde x$, $\tilde y$,
%$\ldots$, to denote (possibly empty) sequences of names.
The class of \ccsb processes is described by the following
grammar:
\[
%\begin{array}{llllll}
P \ ::=\  \nil\ \ \mid\ \ a.P\ \ \mid\ \ \outC{a}\ \ \mid\ \
          P \parallel P\ \ \mid\ \
          !\, P %\vspace*{1.5mm} 
%\end{array}
\]
\end{definition}

ADD PASSIVATION

The term $\nil$ denotes the empty process.
While the
term $a.P$ has the ability to perform the input action $a$,
and then behaves like $P$, 
the term $\outC{a}$ represents an asynchronous output on $a$.
%(which is either the unobservable $\tau$ action or a synchronization on a channel $x$) 
%Two forms of synchronizing action are available, the output $\bar x$ or the input $x$.
%The sum construct $+$ is used to make choice between the summands while
Parallel composition $\parallel $ is used to run parallel programs.
%Restriction $(\nu x)P$ makes the name $x$ local in $P$.
%We denote the process $\alpha.\nullo$ simply with $\alpha$,
%and the process $(\nu x_1)(\nu x_2)\ldots(\nu x_n)P$ with
%$(\nu \tilde x)P$ where $\tilde x$
%is the sequence of names $x_1,x_2,\ldots,x_n$.

% 
% %%%%%%%%%%%%%%% Semantica operazionale %%%%%%%%%%%%%%%%%%
% \begin{table}[t]
% \hrulefill
%   \[
%   {\renewcommand{\arraystretch}{2}
%   \begin{array}{l l@{\hspace{2mm}}
%                 l l@{\hspace{5mm}} }
% \multicolumn{4}{c}{
% 
%     {\tt PRE:}
%     \ \ \ \
%     \alpha.P \stackrel{\alpha}{\longrightarrow} P
%     \ \ \ \ \ \ \ \ \ \ \
%     {\tt PAR:}
%     \ \ \ \
%     \indrule
%     {P \stackrel{\alpha}{\longrightarrow} P'}
%     {P|Q \stackrel{\alpha}{\longrightarrow} P'|Q}
%     \ \ \ \ \ \ \ \ \ \ \
%     {\tt SUM:}
%     \ \ \ \
%     \indrule
%     {P \stackrel{\alpha}{\longrightarrow} P'}
%     {P+Q \stackrel{\alpha}{\longrightarrow} P'}
% }
% \\
% \\
%     {\tt RES:}\ \ \
%     &
%     \indrule
%     {P \stackrel{\alpha}{\longrightarrow} P'}
%     {(\nu x)P \stackrel{\alpha}{\longrightarrow} (\nu x)P'}\
%     \ x \not\in n(\alpha)\ \ \ \
%     &
%     \ \ \ \  \ \ \ \ {\tt COM:}
%     &
%     \indrule
%     {P \stackrel{\alpha}{\longrightarrow} P'\ \ \
%      Q \stackrel{\bar\alpha}{\longrightarrow} Q'}
%     {P|Q \stackrel{\tau}{\longrightarrow} P'|Q'}
% 
% 
%   \vspace*{-5mm}
% 
%   \\
%   &
%   \\
% 
% 
%   \end{array}}
%   \]
% \hrulefill
%   \caption{The transition system for finite core CCS
%            (symmetric rules of {\tt PAR}, {\tt SUM}, and {\tt COM}
%             omitted).}
%   \label{semantica}
% \end{table}
% 
% 
% %The possible prefixes $\alpha$ are the silent action $\tau$,
% %the input action $x$ and the output action $\bar{x}$.
% For input and output actions, we write $\bar \alpha$ for the complementary of $\alpha$;
% that is, if $\alpha = x$
% then $\bar \alpha = \bar x$,
% if $\alpha = \bar x$ then
% $\bar \alpha = x$.
% We write $\fn(P)$, $\bn(P)$ for the
% {\em free names} and the {\em bound names} of $P$.
% The {\em names} of $P$, written $n(P)$,
% is the union of the free and bound names of $P$.
% The names in a label $\alpha$, written $n(\alpha)$
% is the set of names in $\alpha$, i.e. the empty set
% if $\alpha = \tau$ or the singleton $\{x\}$ if
% $\alpha$ is either $x$ or $\bar x$.
% %
% Table~\ref{semantica} contains the set of the transition
% rules for finite CCS.
% 
% \begin{definition}\label{secondadef}
% {\bf (CCS$_{D}$)}
% We assume a denumerable set of constants, ranged over by $D$.
% %Each constant has a non-negative arity.
% The class of CCS$_{D}$ processes is defined by adding the
% production $P \ ::= \ D$
% %\[
% %\begin{array}{lll}
% %P \ ::= \ D \langle \tilde x \rangle
% %\\
% %\end{array}
% %\]
% to the grammar of Definition~\ref{primadef}.
% It is assumed that each constant $D$ has a unique
% defining equation of the form $D \eqdef P$.
% %,
% %where $(\tilde x)$ is a binder for the names
% %in the sequence of names in $\tilde x$.
% %We assume that
% %the names in $\tilde x$ are pairwise distinct.
% %Both in a constant definition $D \eqdef (\tilde x)P$
% %and in a constant application $D \langle \tilde x \rangle$,
% %the parameter $\tilde x$ is a tuple of all distinct names.
% % whose length
% %equals the arity of $D$.
% %As usual, in case the sequence $\tilde x$ is empty,
% %we omit the surrounding parentheses.
% %Moreover, we assume that
% %$fn(P) \subseteq n(\tilde x)$ where $n(\tilde x)$ denotes
% %the set of names in the sequence $\tilde x$.
% \end{definition}
% 
% The transition rule for constant is
% \[
% {\tt CONST:}
% \ \ \ \ \ \
%     \indrule
%     {P \stackrel{\alpha}{\longrightarrow} P'\ \ \ \ \ \ \ \ D \eqdef P}
%     {D  \stackrel{\alpha}{\longrightarrow} P'}
% \]
% %where $P \{\tilde x / \tilde y\}$ is the term obtained by replacing
% %all the free occurrences of the names in $\tilde y$ with the corresponding
% %names in $\tilde x$.
% It is worth noting that this rule for the semantics of constants
% has been adopted also in~\cite{GSV04}. In that paper, it is observed
% that no $\alpha$-conversion is to be considered in calculi
% with this form of constant definition, and this causes name captures 
% and scoping to be dynamic.
% 
% \begin{definition}\label{terzadef}
% {\bf (CCS$_!$)}
% The class of CCS$_!$ processes is defined by adding the production
% $P \ ::= \ \ !P$
% %\[
% %\begin{array}{lll}
% %P \ ::= \ \ !P
% %\end{array}
% %\]
% to the grammar of Definition~\ref{primadef}.
% \end{definition}
% 
% The transition rule for replication is
% \[{\tt REPL:}
% \ \ \ \ \ \     \indrule
%     {P\ |\ !P \stackrel{\alpha}{\longrightarrow} P'}
%     {!P \stackrel{\alpha}{\longrightarrow} P'}
% \]
% %plus its symmetric rule.

\subsection{Undecidability of convergence in $\ccsb$}


\input{ccs-term}
